[Merged by Bors] - chore: move results from `unitary` namespace to `Unitary` #30697

themathqueen · 2025-10-19T20:03:13Z

All results living in the unitary namespace is now in the Unitary namespace.

And the results unitary.spectrum.unitary_conjugate and unitary.spectrum.unitary_conjugate' are renamed to Unitary.spectrum_star_conjugate_left and Unitary.spectrum_star_conjugate_right to match the renaming convention in #30692.

github-actions · 2025-10-19T20:04:30Z

PR summary b8aaf14a89

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Unitary.argSelfAdjoint
+ Unitary.continuousOn_argSelfAdjoint
+ Unitary.expUnitary_eq_mul_inv
+ Unitary.instLocPathConnectedSpace
+ Unitary.inv_mem
+ Unitary.inv_mem_iff
+ Unitary.isPathConnected_ball
+ Unitary.joined
+ Unitary.mem_pathComponentOne_iff
+ Unitary.norm_argSelfAdjoint
+ Unitary.norm_argSelfAdjoint_le_pi
+ Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le
+ Unitary.norm_sub_eq
+ Unitary.norm_sub_one_lt_two_iff
+ Unitary.norm_sub_one_sq_eq
+ Unitary.openPartialHomeomorph
+ Unitary.path
+ Unitary.spectrum_subset_circle
+ Unitary.spectrum_subset_slitPlane_iff_norm_lt_two
+ Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint
+ Unitary.two_mul_one_sub_le_norm_sub_one_sq
+ coe_div
+ coe_inv
+ coe_map
+ coe_map_star
+ coe_mul_star_self
+ coe_neg
+ coe_smul
+ coe_star
+ coe_star_mul_self
+ coe_zpow
+ inner_map_map
+ inv_mem
+ inv_mul_mem_iff
+ linearIsometryEquiv
+ linearIsometryEquiv_coe_apply
+ linearIsometryEquiv_coe_symm_apply
+ map
+ mapEquiv
+ mapEquiv_refl
+ mapEquiv_symm
+ mapEquiv_trans
+ map_comp
+ map_id
+ map_injective
+ map_mem
+ mem_iff
+ mem_iff_self_mul_star
+ mem_iff_star_mul_self
+ mul_inv_mem_iff
+ mul_left_inj
+ mul_right_inj
+ mul_star_self
+ mul_star_self_of_mem
+ norm_map
+ smul_mem
+ smul_mem_of_mem
+ spectrum_star_left_conjugate
+ spectrum_star_right_conjugate
+ star_eq_inv
+ star_eq_inv'
+ star_mem
+ star_mem_iff
+ star_mul_self
+ star_mul_self_of_mem
+ toMonoidHom_mapEquiv
+ toUnits
+ toUnits_comp_map
+ toUnits_injective
+ val_toUnits_apply
- unitary.instLocPathConnectedSpace
- unitary.inv_mem
- unitary.inv_mem_iff
- unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mark unitary_conjugate and unitary_conjugate' as deprecated.

Mathlib/Algebra/Star/Unitary.lean

riccardobrasca · 2025-10-27T08:00:25Z

Maybe it should be called unitary.spectrum_conjugate? And why the u is lowercase?!

themathqueen · 2025-10-27T11:37:29Z

Maybe it should be called unitary.spectrum_conjugate?

Sure, but how about unitary.spectrum_star_right_conjugate (and _left_ for the primed version)?

And why the u is lowercase?!

Not sure, I changed it now lol.

riccardobrasca · 2025-10-29T18:31:36Z

All results in this file about unitary matrices should just be in the Unitary namespace in my opinion.

themathqueen · 2025-10-29T19:00:21Z

All results in this file about unitary matrices should just be in the Unitary namespace in my opinion.

I changed it so that they're in the unitary namespace like the rest of the file.

themathqueen · 2025-10-29T19:01:48Z

But about unitary vs Unitary, I think that's out of scope for this pr. That would be a much larger pr, I presume.

riccardobrasca · 2025-10-29T19:04:43Z

Can you just try? Maybe it's enough to capitalize a u in this file and in a couple of open lines.

themathqueen · 2025-10-29T20:21:46Z

Alright, @riccardobrasca, done. See how big this pr is now 😭. But oh well, it didn't take nearly as long as I thought.

riccardobrasca · 2025-10-29T20:34:46Z

LGTM, thanks a lot!

bors d+

mathlib-bors · 2025-10-29T20:34:48Z

✌️ themathqueen can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

…together

themathqueen · 2025-10-29T20:47:49Z

bors r+

All results living in the `unitary` namespace is now in the `Unitary` namespace. And the results `unitary.spectrum.unitary_conjugate` and `unitary.spectrum.unitary_conjugate'` are renamed to `Unitary.spectrum_star_conjugate_left` and `Unitary.spectrum_star_conjugate_right` to match the renaming convention in #30692.

mathlib-bors · 2025-10-29T21:39:27Z

Pull request successfully merged into master.

Build succeeded:

fix lemma names

e9c13a0

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 19, 2025

themathqueen added the easy < 20s of review time. See the lifecycle page for guidelines. label Oct 19, 2025

themathqueen and others added 4 commits October 19, 2025 20:15

fix

eeb5b96

Deprecate unitary_conjugate aliases

3239f1d

Mark unitary_conjugate and unitary_conjugate' as deprecated.

Update Unitary.lean

d22e8f8

Apply suggestions from code review

b345780

themathqueen commented Oct 20, 2025

View reviewed changes

Mathlib/Algebra/Star/Unitary.lean Outdated Show resolved Hide resolved

Update Mathlib/Algebra/Star/Unitary.lean

a81d974

themathqueen changed the title ~~chore(Algebra/Star/Unitary): fix lemma names~~ chore(Algebra/Star/Unitary): rename unitary.spectrum.unitary_conjugate Oct 20, 2025

themathqueen commented Oct 20, 2025

View reviewed changes

Mathlib/Algebra/Star/Unitary.lean Outdated Show resolved Hide resolved

Update Mathlib/Algebra/Star/Unitary.lean

3870b0b

themathqueen commented Oct 20, 2025

View reviewed changes

Mathlib/Algebra/Star/Unitary.lean Outdated Show resolved Hide resolved

themathqueen commented Oct 20, 2025

View reviewed changes

Mathlib/Algebra/Star/Unitary.lean Show resolved Hide resolved

Apply suggestions from code review

c38d728

leanprover-community-bot-assistant assigned riccardobrasca Oct 27, 2025

Update Unitary.lean

cc17fe9

Merge branch 'master' into chore_unitary_rename

f11d0db

jcommelin removed the easy < 20s of review time. See the lifecycle page for guidelines. label Oct 28, 2025

themathqueen added 2 commits October 29, 2025 18:57

Update Unitary.lean

6467c98

Update HermitianFunctionalCalculus.lean

accebf5

themathqueen added 2 commits October 29, 2025 19:29

unitary -> Unitary

2823bc3

fixes

87b844d

last file?

320278e

themathqueen changed the title ~~chore(Algebra/Star/Unitary): rename unitary.spectrum.unitary_conjugate~~ chore(Algebra/Star/Unitary): move results from unitary namespace to Unitary Oct 29, 2025

themathqueen added 4 commits October 29, 2025 19:54

2 more files

76250e0

two more files

b52999c

last result

d25b796

cleanup

e7a70ec

themathqueen changed the title ~~chore(Algebra/Star/Unitary): move results from unitary namespace to Unitary~~ chore: move results from unitary namespace to Unitary Oct 29, 2025

Merge branch 'master' into chore_unitary_rename

83bbedb

leanprover-community-mathlib4-bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 29, 2025

add a section title for deprecated results since they're all grouped …

378ac78

…together

mathlib-bors bot changed the title ~~chore: move results from unitary namespace to Unitary~~ [Merged by Bors] - chore: move results from unitary namespace to Unitary Oct 29, 2025

mathlib-bors bot closed this Oct 29, 2025

themathqueen deleted the chore_unitary_rename branch October 29, 2025 21:40

Uh oh!

[Merged by Bors] - chore: move results from unitary namespace to Unitary #30697

[Merged by Bors] - chore: move results from unitary namespace to Unitary #30697

Conversation

themathqueen commented Oct 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary b8aaf14a89

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

riccardobrasca commented Oct 27, 2025

Uh oh!

themathqueen commented Oct 27, 2025

Uh oh!

riccardobrasca commented Oct 29, 2025

Uh oh!

themathqueen commented Oct 29, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

themathqueen commented Oct 29, 2025

Uh oh!

riccardobrasca commented Oct 29, 2025

Uh oh!

themathqueen commented Oct 29, 2025

Uh oh!

riccardobrasca commented Oct 29, 2025

Uh oh!

mathlib-bors bot commented Oct 29, 2025

Uh oh!

themathqueen commented Oct 29, 2025

Uh oh!

mathlib-bors bot commented Oct 29, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

[Merged by Bors] - chore: move results from `unitary` namespace to `Unitary` #30697

[Merged by Bors] - chore: move results from `unitary` namespace to `Unitary` #30697

themathqueen commented Oct 19, 2025 •

edited

Loading

github-actions bot commented Oct 19, 2025 •

edited

Loading

themathqueen commented Oct 29, 2025 •

edited

Loading